(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
0(0(0(x1))) → 0(0(1(0(2(x1)))))
0(3(2(x1))) → 4(3(0(2(x1))))
0(0(4(2(x1)))) → 0(4(1(0(2(x1)))))
0(0(5(2(x1)))) → 5(0(2(3(0(x1)))))
0(1(3(2(x1)))) → 0(3(1(0(2(x1)))))
0(1(3(2(x1)))) → 3(1(1(0(2(x1)))))
0(1(3(2(x1)))) → 0(1(4(3(1(2(x1))))))
0(4(1(3(x1)))) → 1(4(3(0(2(2(x1))))))
0(4(2(3(x1)))) → 5(4(3(0(2(x1)))))
0(4(5(2(x1)))) → 5(0(2(2(4(2(x1))))))
0(5(1(3(x1)))) → 3(0(1(5(1(2(x1))))))
0(5(3(0(x1)))) → 5(0(1(4(3(0(x1))))))
0(5(3(2(x1)))) → 5(1(5(0(2(3(x1))))))
4(0(2(3(x1)))) → 3(4(3(0(2(x1)))))
4(0(2(3(x1)))) → 4(3(5(0(2(x1)))))
4(4(1(3(x1)))) → 4(3(4(1(2(2(x1))))))
4(5(2(0(x1)))) → 4(2(1(5(0(2(x1))))))
4(5(2(0(x1)))) → 5(1(0(2(2(4(x1))))))
5(1(0(0(x1)))) → 5(1(0(2(0(x1)))))
5(1(0(0(x1)))) → 5(2(1(0(2(0(x1))))))
5(1(3(0(x1)))) → 5(0(2(1(3(x1)))))
5(1(3(2(x1)))) → 3(0(1(5(1(2(x1))))))
5(1(3(2(x1)))) → 3(1(1(5(2(2(x1))))))
5(3(0(0(x1)))) → 5(0(4(3(0(2(x1))))))
0(0(4(1(3(x1))))) → 4(0(1(0(2(3(x1))))))
0(0(4(5(2(x1))))) → 5(0(1(0(2(4(x1))))))
0(0(5(3(2(x1))))) → 0(1(5(0(2(3(x1))))))
0(1(0(5(2(x1))))) → 1(0(2(5(1(0(x1))))))
0(1(4(5(2(x1))))) → 2(1(5(0(2(4(x1))))))
0(3(1(4(0(x1))))) → 4(1(0(1(0(3(x1))))))
0(3(2(0(0(x1))))) → 0(0(1(0(2(3(x1))))))
0(3(4(0(2(x1))))) → 4(3(0(2(1(0(x1))))))
0(3(4(0(2(x1))))) → 4(3(0(2(3(0(x1))))))
0(3(4(4(2(x1))))) → 4(0(3(4(2(2(x1))))))
0(4(2(5(3(x1))))) → 0(4(3(5(1(2(x1))))))
0(5(1(2(0(x1))))) → 3(0(1(5(0(2(x1))))))
4(4(2(2(0(x1))))) → 4(1(0(2(2(4(x1))))))
4(5(1(2(0(x1))))) → 5(0(4(1(2(2(x1))))))
4(5(2(3(2(x1))))) → 5(4(3(5(2(2(x1))))))
5(1(0(3(2(x1))))) → 5(0(3(1(0(2(x1))))))
5(1(0(5(3(x1))))) → 5(5(0(1(3(1(x1))))))
5(1(3(0(0(x1))))) → 3(5(0(1(2(0(x1))))))
5(1(3(0(2(x1))))) → 3(0(2(1(5(2(x1))))))
5(1(3(0(2(x1))))) → 5(0(1(0(3(2(x1))))))
5(1(3(0(2(x1))))) → 5(0(1(1(2(3(x1))))))
5(1(3(2(0(x1))))) → 5(3(1(5(2(0(x1))))))
5(1(3(2(3(x1))))) → 3(4(3(5(1(2(x1))))))
5(1(4(5(2(x1))))) → 5(1(4(1(5(2(x1))))))
5(5(1(3(2(x1))))) → 3(5(5(4(1(2(x1))))))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(0(0(z0))) → 0(0(1(0(2(z0)))))
0(3(2(z0))) → 4(3(0(2(z0))))
0(0(4(2(z0)))) → 0(4(1(0(2(z0)))))
0(0(5(2(z0)))) → 5(0(2(3(0(z0)))))
0(1(3(2(z0)))) → 0(3(1(0(2(z0)))))
0(1(3(2(z0)))) → 3(1(1(0(2(z0)))))
0(1(3(2(z0)))) → 0(1(4(3(1(2(z0))))))
0(4(1(3(z0)))) → 1(4(3(0(2(2(z0))))))
0(4(2(3(z0)))) → 5(4(3(0(2(z0)))))
0(4(5(2(z0)))) → 5(0(2(2(4(2(z0))))))
0(5(1(3(z0)))) → 3(0(1(5(1(2(z0))))))
0(5(3(0(z0)))) → 5(0(1(4(3(0(z0))))))
0(5(3(2(z0)))) → 5(1(5(0(2(3(z0))))))
0(0(4(1(3(z0))))) → 4(0(1(0(2(3(z0))))))
0(0(4(5(2(z0))))) → 5(0(1(0(2(4(z0))))))
0(0(5(3(2(z0))))) → 0(1(5(0(2(3(z0))))))
0(1(0(5(2(z0))))) → 1(0(2(5(1(0(z0))))))
0(1(4(5(2(z0))))) → 2(1(5(0(2(4(z0))))))
0(3(1(4(0(z0))))) → 4(1(0(1(0(3(z0))))))
0(3(2(0(0(z0))))) → 0(0(1(0(2(3(z0))))))
0(3(4(0(2(z0))))) → 4(3(0(2(1(0(z0))))))
0(3(4(0(2(z0))))) → 4(3(0(2(3(0(z0))))))
0(3(4(4(2(z0))))) → 4(0(3(4(2(2(z0))))))
0(4(2(5(3(z0))))) → 0(4(3(5(1(2(z0))))))
0(5(1(2(0(z0))))) → 3(0(1(5(0(2(z0))))))
4(0(2(3(z0)))) → 3(4(3(0(2(z0)))))
4(0(2(3(z0)))) → 4(3(5(0(2(z0)))))
4(4(1(3(z0)))) → 4(3(4(1(2(2(z0))))))
4(5(2(0(z0)))) → 4(2(1(5(0(2(z0))))))
4(5(2(0(z0)))) → 5(1(0(2(2(4(z0))))))
4(4(2(2(0(z0))))) → 4(1(0(2(2(4(z0))))))
4(5(1(2(0(z0))))) → 5(0(4(1(2(2(z0))))))
4(5(2(3(2(z0))))) → 5(4(3(5(2(2(z0))))))
5(1(0(0(z0)))) → 5(1(0(2(0(z0)))))
5(1(0(0(z0)))) → 5(2(1(0(2(0(z0))))))
5(1(3(0(z0)))) → 5(0(2(1(3(z0)))))
5(1(3(2(z0)))) → 3(0(1(5(1(2(z0))))))
5(1(3(2(z0)))) → 3(1(1(5(2(2(z0))))))
5(3(0(0(z0)))) → 5(0(4(3(0(2(z0))))))
5(1(0(3(2(z0))))) → 5(0(3(1(0(2(z0))))))
5(1(0(5(3(z0))))) → 5(5(0(1(3(1(z0))))))
5(1(3(0(0(z0))))) → 3(5(0(1(2(0(z0))))))
5(1(3(0(2(z0))))) → 3(0(2(1(5(2(z0))))))
5(1(3(0(2(z0))))) → 5(0(1(0(3(2(z0))))))
5(1(3(0(2(z0))))) → 5(0(1(1(2(3(z0))))))
5(1(3(2(0(z0))))) → 5(3(1(5(2(0(z0))))))
5(1(3(2(3(z0))))) → 3(4(3(5(1(2(z0))))))
5(1(4(5(2(z0))))) → 5(1(4(1(5(2(z0))))))
5(5(1(3(2(z0))))) → 3(5(5(4(1(2(z0))))))
Tuples:
0'(0(0(z0))) → c(0'(0(1(0(2(z0))))), 0'(1(0(2(z0)))), 0'(2(z0)))
0'(3(2(z0))) → c1(4'(3(0(2(z0)))), 0'(2(z0)))
0'(0(4(2(z0)))) → c2(0'(4(1(0(2(z0))))), 4'(1(0(2(z0)))), 0'(2(z0)))
0'(0(5(2(z0)))) → c3(5'(0(2(3(0(z0))))), 0'(2(3(0(z0)))), 0'(z0))
0'(1(3(2(z0)))) → c4(0'(3(1(0(2(z0))))), 0'(2(z0)))
0'(1(3(2(z0)))) → c5(0'(2(z0)))
0'(1(3(2(z0)))) → c6(0'(1(4(3(1(2(z0)))))), 4'(3(1(2(z0)))))
0'(4(1(3(z0)))) → c7(4'(3(0(2(2(z0))))), 0'(2(2(z0))))
0'(4(2(3(z0)))) → c8(5'(4(3(0(2(z0))))), 4'(3(0(2(z0)))), 0'(2(z0)))
0'(4(5(2(z0)))) → c9(5'(0(2(2(4(2(z0)))))), 0'(2(2(4(2(z0))))), 4'(2(z0)))
0'(5(1(3(z0)))) → c10(0'(1(5(1(2(z0))))), 5'(1(2(z0))))
0'(5(3(0(z0)))) → c11(5'(0(1(4(3(0(z0)))))), 0'(1(4(3(0(z0))))), 4'(3(0(z0))), 0'(z0))
0'(5(3(2(z0)))) → c12(5'(1(5(0(2(3(z0)))))), 5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(0(4(1(3(z0))))) → c13(4'(0(1(0(2(3(z0)))))), 0'(1(0(2(3(z0))))), 0'(2(3(z0))))
0'(0(4(5(2(z0))))) → c14(5'(0(1(0(2(4(z0)))))), 0'(1(0(2(4(z0))))), 0'(2(4(z0))), 4'(z0))
0'(0(5(3(2(z0))))) → c15(0'(1(5(0(2(3(z0)))))), 5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(1(0(5(2(z0))))) → c16(0'(2(5(1(0(z0))))), 5'(1(0(z0))), 0'(z0))
0'(1(4(5(2(z0))))) → c17(5'(0(2(4(z0)))), 0'(2(4(z0))), 4'(z0))
0'(3(1(4(0(z0))))) → c18(4'(1(0(1(0(3(z0)))))), 0'(1(0(3(z0)))), 0'(3(z0)))
0'(3(2(0(0(z0))))) → c19(0'(0(1(0(2(3(z0)))))), 0'(1(0(2(3(z0))))), 0'(2(3(z0))))
0'(3(4(0(2(z0))))) → c20(4'(3(0(2(1(0(z0)))))), 0'(2(1(0(z0)))), 0'(z0))
0'(3(4(0(2(z0))))) → c21(4'(3(0(2(3(0(z0)))))), 0'(2(3(0(z0)))), 0'(z0))
0'(3(4(4(2(z0))))) → c22(4'(0(3(4(2(2(z0)))))), 0'(3(4(2(2(z0))))), 4'(2(2(z0))))
0'(4(2(5(3(z0))))) → c23(0'(4(3(5(1(2(z0)))))), 4'(3(5(1(2(z0))))), 5'(1(2(z0))))
0'(5(1(2(0(z0))))) → c24(0'(1(5(0(2(z0))))), 5'(0(2(z0))), 0'(2(z0)))
4'(0(2(3(z0)))) → c25(4'(3(0(2(z0)))), 0'(2(z0)))
4'(0(2(3(z0)))) → c26(4'(3(5(0(2(z0))))), 5'(0(2(z0))), 0'(2(z0)))
4'(4(1(3(z0)))) → c27(4'(3(4(1(2(2(z0)))))), 4'(1(2(2(z0)))))
4'(5(2(0(z0)))) → c28(4'(2(1(5(0(2(z0)))))), 5'(0(2(z0))), 0'(2(z0)))
4'(5(2(0(z0)))) → c29(5'(1(0(2(2(4(z0)))))), 0'(2(2(4(z0)))), 4'(z0))
4'(4(2(2(0(z0))))) → c30(4'(1(0(2(2(4(z0)))))), 0'(2(2(4(z0)))), 4'(z0))
4'(5(1(2(0(z0))))) → c31(5'(0(4(1(2(2(z0)))))), 0'(4(1(2(2(z0))))), 4'(1(2(2(z0)))))
4'(5(2(3(2(z0))))) → c32(5'(4(3(5(2(2(z0)))))), 4'(3(5(2(2(z0))))), 5'(2(2(z0))))
5'(1(0(0(z0)))) → c33(5'(1(0(2(0(z0))))), 0'(2(0(z0))), 0'(z0))
5'(1(0(0(z0)))) → c34(5'(2(1(0(2(0(z0)))))), 0'(2(0(z0))), 0'(z0))
5'(1(3(0(z0)))) → c35(5'(0(2(1(3(z0))))), 0'(2(1(3(z0)))))
5'(1(3(2(z0)))) → c36(0'(1(5(1(2(z0))))), 5'(1(2(z0))))
5'(1(3(2(z0)))) → c37(5'(2(2(z0))))
5'(3(0(0(z0)))) → c38(5'(0(4(3(0(2(z0)))))), 0'(4(3(0(2(z0))))), 4'(3(0(2(z0)))), 0'(2(z0)))
5'(1(0(3(2(z0))))) → c39(5'(0(3(1(0(2(z0)))))), 0'(3(1(0(2(z0))))), 0'(2(z0)))
5'(1(0(5(3(z0))))) → c40(5'(5(0(1(3(1(z0)))))), 5'(0(1(3(1(z0))))), 0'(1(3(1(z0)))))
5'(1(3(0(0(z0))))) → c41(5'(0(1(2(0(z0))))), 0'(1(2(0(z0)))), 0'(z0))
5'(1(3(0(2(z0))))) → c42(0'(2(1(5(2(z0))))), 5'(2(z0)))
5'(1(3(0(2(z0))))) → c43(5'(0(1(0(3(2(z0)))))), 0'(1(0(3(2(z0))))), 0'(3(2(z0))))
5'(1(3(0(2(z0))))) → c44(5'(0(1(1(2(3(z0)))))), 0'(1(1(2(3(z0))))))
5'(1(3(2(0(z0))))) → c45(5'(3(1(5(2(0(z0)))))), 5'(2(0(z0))), 0'(z0))
5'(1(3(2(3(z0))))) → c46(4'(3(5(1(2(z0))))), 5'(1(2(z0))))
5'(1(4(5(2(z0))))) → c47(5'(1(4(1(5(2(z0)))))), 4'(1(5(2(z0)))), 5'(2(z0)))
5'(5(1(3(2(z0))))) → c48(5'(5(4(1(2(z0))))), 5'(4(1(2(z0)))), 4'(1(2(z0))))
S tuples:
0'(0(0(z0))) → c(0'(0(1(0(2(z0))))), 0'(1(0(2(z0)))), 0'(2(z0)))
0'(3(2(z0))) → c1(4'(3(0(2(z0)))), 0'(2(z0)))
0'(0(4(2(z0)))) → c2(0'(4(1(0(2(z0))))), 4'(1(0(2(z0)))), 0'(2(z0)))
0'(0(5(2(z0)))) → c3(5'(0(2(3(0(z0))))), 0'(2(3(0(z0)))), 0'(z0))
0'(1(3(2(z0)))) → c4(0'(3(1(0(2(z0))))), 0'(2(z0)))
0'(1(3(2(z0)))) → c5(0'(2(z0)))
0'(1(3(2(z0)))) → c6(0'(1(4(3(1(2(z0)))))), 4'(3(1(2(z0)))))
0'(4(1(3(z0)))) → c7(4'(3(0(2(2(z0))))), 0'(2(2(z0))))
0'(4(2(3(z0)))) → c8(5'(4(3(0(2(z0))))), 4'(3(0(2(z0)))), 0'(2(z0)))
0'(4(5(2(z0)))) → c9(5'(0(2(2(4(2(z0)))))), 0'(2(2(4(2(z0))))), 4'(2(z0)))
0'(5(1(3(z0)))) → c10(0'(1(5(1(2(z0))))), 5'(1(2(z0))))
0'(5(3(0(z0)))) → c11(5'(0(1(4(3(0(z0)))))), 0'(1(4(3(0(z0))))), 4'(3(0(z0))), 0'(z0))
0'(5(3(2(z0)))) → c12(5'(1(5(0(2(3(z0)))))), 5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(0(4(1(3(z0))))) → c13(4'(0(1(0(2(3(z0)))))), 0'(1(0(2(3(z0))))), 0'(2(3(z0))))
0'(0(4(5(2(z0))))) → c14(5'(0(1(0(2(4(z0)))))), 0'(1(0(2(4(z0))))), 0'(2(4(z0))), 4'(z0))
0'(0(5(3(2(z0))))) → c15(0'(1(5(0(2(3(z0)))))), 5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(1(0(5(2(z0))))) → c16(0'(2(5(1(0(z0))))), 5'(1(0(z0))), 0'(z0))
0'(1(4(5(2(z0))))) → c17(5'(0(2(4(z0)))), 0'(2(4(z0))), 4'(z0))
0'(3(1(4(0(z0))))) → c18(4'(1(0(1(0(3(z0)))))), 0'(1(0(3(z0)))), 0'(3(z0)))
0'(3(2(0(0(z0))))) → c19(0'(0(1(0(2(3(z0)))))), 0'(1(0(2(3(z0))))), 0'(2(3(z0))))
0'(3(4(0(2(z0))))) → c20(4'(3(0(2(1(0(z0)))))), 0'(2(1(0(z0)))), 0'(z0))
0'(3(4(0(2(z0))))) → c21(4'(3(0(2(3(0(z0)))))), 0'(2(3(0(z0)))), 0'(z0))
0'(3(4(4(2(z0))))) → c22(4'(0(3(4(2(2(z0)))))), 0'(3(4(2(2(z0))))), 4'(2(2(z0))))
0'(4(2(5(3(z0))))) → c23(0'(4(3(5(1(2(z0)))))), 4'(3(5(1(2(z0))))), 5'(1(2(z0))))
0'(5(1(2(0(z0))))) → c24(0'(1(5(0(2(z0))))), 5'(0(2(z0))), 0'(2(z0)))
4'(0(2(3(z0)))) → c25(4'(3(0(2(z0)))), 0'(2(z0)))
4'(0(2(3(z0)))) → c26(4'(3(5(0(2(z0))))), 5'(0(2(z0))), 0'(2(z0)))
4'(4(1(3(z0)))) → c27(4'(3(4(1(2(2(z0)))))), 4'(1(2(2(z0)))))
4'(5(2(0(z0)))) → c28(4'(2(1(5(0(2(z0)))))), 5'(0(2(z0))), 0'(2(z0)))
4'(5(2(0(z0)))) → c29(5'(1(0(2(2(4(z0)))))), 0'(2(2(4(z0)))), 4'(z0))
4'(4(2(2(0(z0))))) → c30(4'(1(0(2(2(4(z0)))))), 0'(2(2(4(z0)))), 4'(z0))
4'(5(1(2(0(z0))))) → c31(5'(0(4(1(2(2(z0)))))), 0'(4(1(2(2(z0))))), 4'(1(2(2(z0)))))
4'(5(2(3(2(z0))))) → c32(5'(4(3(5(2(2(z0)))))), 4'(3(5(2(2(z0))))), 5'(2(2(z0))))
5'(1(0(0(z0)))) → c33(5'(1(0(2(0(z0))))), 0'(2(0(z0))), 0'(z0))
5'(1(0(0(z0)))) → c34(5'(2(1(0(2(0(z0)))))), 0'(2(0(z0))), 0'(z0))
5'(1(3(0(z0)))) → c35(5'(0(2(1(3(z0))))), 0'(2(1(3(z0)))))
5'(1(3(2(z0)))) → c36(0'(1(5(1(2(z0))))), 5'(1(2(z0))))
5'(1(3(2(z0)))) → c37(5'(2(2(z0))))
5'(3(0(0(z0)))) → c38(5'(0(4(3(0(2(z0)))))), 0'(4(3(0(2(z0))))), 4'(3(0(2(z0)))), 0'(2(z0)))
5'(1(0(3(2(z0))))) → c39(5'(0(3(1(0(2(z0)))))), 0'(3(1(0(2(z0))))), 0'(2(z0)))
5'(1(0(5(3(z0))))) → c40(5'(5(0(1(3(1(z0)))))), 5'(0(1(3(1(z0))))), 0'(1(3(1(z0)))))
5'(1(3(0(0(z0))))) → c41(5'(0(1(2(0(z0))))), 0'(1(2(0(z0)))), 0'(z0))
5'(1(3(0(2(z0))))) → c42(0'(2(1(5(2(z0))))), 5'(2(z0)))
5'(1(3(0(2(z0))))) → c43(5'(0(1(0(3(2(z0)))))), 0'(1(0(3(2(z0))))), 0'(3(2(z0))))
5'(1(3(0(2(z0))))) → c44(5'(0(1(1(2(3(z0)))))), 0'(1(1(2(3(z0))))))
5'(1(3(2(0(z0))))) → c45(5'(3(1(5(2(0(z0)))))), 5'(2(0(z0))), 0'(z0))
5'(1(3(2(3(z0))))) → c46(4'(3(5(1(2(z0))))), 5'(1(2(z0))))
5'(1(4(5(2(z0))))) → c47(5'(1(4(1(5(2(z0)))))), 4'(1(5(2(z0)))), 5'(2(z0)))
5'(5(1(3(2(z0))))) → c48(5'(5(4(1(2(z0))))), 5'(4(1(2(z0)))), 4'(1(2(z0))))
K tuples:none
Defined Rule Symbols:
0, 4, 5
Defined Pair Symbols:
0', 4', 5'
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
0'(0(0(z0))) → c(0'(0(1(0(2(z0))))), 0'(1(0(2(z0)))), 0'(2(z0)))
0'(0(4(2(z0)))) → c2(0'(4(1(0(2(z0))))), 4'(1(0(2(z0)))), 0'(2(z0)))
0'(0(5(2(z0)))) → c3(5'(0(2(3(0(z0))))), 0'(2(3(0(z0)))), 0'(z0))
0'(4(1(3(z0)))) → c7(4'(3(0(2(2(z0))))), 0'(2(2(z0))))
0'(4(2(3(z0)))) → c8(5'(4(3(0(2(z0))))), 4'(3(0(2(z0)))), 0'(2(z0)))
0'(4(5(2(z0)))) → c9(5'(0(2(2(4(2(z0)))))), 0'(2(2(4(2(z0))))), 4'(2(z0)))
0'(5(1(3(z0)))) → c10(0'(1(5(1(2(z0))))), 5'(1(2(z0))))
0'(5(3(0(z0)))) → c11(5'(0(1(4(3(0(z0)))))), 0'(1(4(3(0(z0))))), 4'(3(0(z0))), 0'(z0))
0'(5(3(2(z0)))) → c12(5'(1(5(0(2(3(z0)))))), 5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(0(4(1(3(z0))))) → c13(4'(0(1(0(2(3(z0)))))), 0'(1(0(2(3(z0))))), 0'(2(3(z0))))
0'(0(4(5(2(z0))))) → c14(5'(0(1(0(2(4(z0)))))), 0'(1(0(2(4(z0))))), 0'(2(4(z0))), 4'(z0))
0'(0(5(3(2(z0))))) → c15(0'(1(5(0(2(3(z0)))))), 5'(0(2(3(z0)))), 0'(2(3(z0))))
0'(1(0(5(2(z0))))) → c16(0'(2(5(1(0(z0))))), 5'(1(0(z0))), 0'(z0))
0'(1(4(5(2(z0))))) → c17(5'(0(2(4(z0)))), 0'(2(4(z0))), 4'(z0))
0'(3(1(4(0(z0))))) → c18(4'(1(0(1(0(3(z0)))))), 0'(1(0(3(z0)))), 0'(3(z0)))
0'(3(2(0(0(z0))))) → c19(0'(0(1(0(2(3(z0)))))), 0'(1(0(2(3(z0))))), 0'(2(3(z0))))
0'(3(4(0(2(z0))))) → c20(4'(3(0(2(1(0(z0)))))), 0'(2(1(0(z0)))), 0'(z0))
0'(3(4(0(2(z0))))) → c21(4'(3(0(2(3(0(z0)))))), 0'(2(3(0(z0)))), 0'(z0))
0'(3(4(4(2(z0))))) → c22(4'(0(3(4(2(2(z0)))))), 0'(3(4(2(2(z0))))), 4'(2(2(z0))))
0'(4(2(5(3(z0))))) → c23(0'(4(3(5(1(2(z0)))))), 4'(3(5(1(2(z0))))), 5'(1(2(z0))))
0'(5(1(2(0(z0))))) → c24(0'(1(5(0(2(z0))))), 5'(0(2(z0))), 0'(2(z0)))
4'(0(2(3(z0)))) → c25(4'(3(0(2(z0)))), 0'(2(z0)))
4'(0(2(3(z0)))) → c26(4'(3(5(0(2(z0))))), 5'(0(2(z0))), 0'(2(z0)))
4'(4(1(3(z0)))) → c27(4'(3(4(1(2(2(z0)))))), 4'(1(2(2(z0)))))
4'(5(2(0(z0)))) → c28(4'(2(1(5(0(2(z0)))))), 5'(0(2(z0))), 0'(2(z0)))
4'(5(2(0(z0)))) → c29(5'(1(0(2(2(4(z0)))))), 0'(2(2(4(z0)))), 4'(z0))
4'(4(2(2(0(z0))))) → c30(4'(1(0(2(2(4(z0)))))), 0'(2(2(4(z0)))), 4'(z0))
4'(5(1(2(0(z0))))) → c31(5'(0(4(1(2(2(z0)))))), 0'(4(1(2(2(z0))))), 4'(1(2(2(z0)))))
4'(5(2(3(2(z0))))) → c32(5'(4(3(5(2(2(z0)))))), 4'(3(5(2(2(z0))))), 5'(2(2(z0))))
5'(1(0(0(z0)))) → c33(5'(1(0(2(0(z0))))), 0'(2(0(z0))), 0'(z0))
5'(1(0(0(z0)))) → c34(5'(2(1(0(2(0(z0)))))), 0'(2(0(z0))), 0'(z0))
5'(1(3(0(z0)))) → c35(5'(0(2(1(3(z0))))), 0'(2(1(3(z0)))))
5'(3(0(0(z0)))) → c38(5'(0(4(3(0(2(z0)))))), 0'(4(3(0(2(z0))))), 4'(3(0(2(z0)))), 0'(2(z0)))
5'(1(0(3(2(z0))))) → c39(5'(0(3(1(0(2(z0)))))), 0'(3(1(0(2(z0))))), 0'(2(z0)))
5'(1(0(5(3(z0))))) → c40(5'(5(0(1(3(1(z0)))))), 5'(0(1(3(1(z0))))), 0'(1(3(1(z0)))))
5'(1(3(0(0(z0))))) → c41(5'(0(1(2(0(z0))))), 0'(1(2(0(z0)))), 0'(z0))
5'(1(3(0(2(z0))))) → c42(0'(2(1(5(2(z0))))), 5'(2(z0)))
5'(1(3(0(2(z0))))) → c43(5'(0(1(0(3(2(z0)))))), 0'(1(0(3(2(z0))))), 0'(3(2(z0))))
5'(1(3(0(2(z0))))) → c44(5'(0(1(1(2(3(z0)))))), 0'(1(1(2(3(z0))))))
5'(1(3(2(0(z0))))) → c45(5'(3(1(5(2(0(z0)))))), 5'(2(0(z0))), 0'(z0))
5'(1(4(5(2(z0))))) → c47(5'(1(4(1(5(2(z0)))))), 4'(1(5(2(z0)))), 5'(2(z0)))
5'(5(1(3(2(z0))))) → c48(5'(5(4(1(2(z0))))), 5'(4(1(2(z0)))), 4'(1(2(z0))))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(0(0(z0))) → 0(0(1(0(2(z0)))))
0(3(2(z0))) → 4(3(0(2(z0))))
0(0(4(2(z0)))) → 0(4(1(0(2(z0)))))
0(0(5(2(z0)))) → 5(0(2(3(0(z0)))))
0(1(3(2(z0)))) → 0(3(1(0(2(z0)))))
0(1(3(2(z0)))) → 3(1(1(0(2(z0)))))
0(1(3(2(z0)))) → 0(1(4(3(1(2(z0))))))
0(4(1(3(z0)))) → 1(4(3(0(2(2(z0))))))
0(4(2(3(z0)))) → 5(4(3(0(2(z0)))))
0(4(5(2(z0)))) → 5(0(2(2(4(2(z0))))))
0(5(1(3(z0)))) → 3(0(1(5(1(2(z0))))))
0(5(3(0(z0)))) → 5(0(1(4(3(0(z0))))))
0(5(3(2(z0)))) → 5(1(5(0(2(3(z0))))))
0(0(4(1(3(z0))))) → 4(0(1(0(2(3(z0))))))
0(0(4(5(2(z0))))) → 5(0(1(0(2(4(z0))))))
0(0(5(3(2(z0))))) → 0(1(5(0(2(3(z0))))))
0(1(0(5(2(z0))))) → 1(0(2(5(1(0(z0))))))
0(1(4(5(2(z0))))) → 2(1(5(0(2(4(z0))))))
0(3(1(4(0(z0))))) → 4(1(0(1(0(3(z0))))))
0(3(2(0(0(z0))))) → 0(0(1(0(2(3(z0))))))
0(3(4(0(2(z0))))) → 4(3(0(2(1(0(z0))))))
0(3(4(0(2(z0))))) → 4(3(0(2(3(0(z0))))))
0(3(4(4(2(z0))))) → 4(0(3(4(2(2(z0))))))
0(4(2(5(3(z0))))) → 0(4(3(5(1(2(z0))))))
0(5(1(2(0(z0))))) → 3(0(1(5(0(2(z0))))))
4(0(2(3(z0)))) → 3(4(3(0(2(z0)))))
4(0(2(3(z0)))) → 4(3(5(0(2(z0)))))
4(4(1(3(z0)))) → 4(3(4(1(2(2(z0))))))
4(5(2(0(z0)))) → 4(2(1(5(0(2(z0))))))
4(5(2(0(z0)))) → 5(1(0(2(2(4(z0))))))
4(4(2(2(0(z0))))) → 4(1(0(2(2(4(z0))))))
4(5(1(2(0(z0))))) → 5(0(4(1(2(2(z0))))))
4(5(2(3(2(z0))))) → 5(4(3(5(2(2(z0))))))
5(1(0(0(z0)))) → 5(1(0(2(0(z0)))))
5(1(0(0(z0)))) → 5(2(1(0(2(0(z0))))))
5(1(3(0(z0)))) → 5(0(2(1(3(z0)))))
5(1(3(2(z0)))) → 3(0(1(5(1(2(z0))))))
5(1(3(2(z0)))) → 3(1(1(5(2(2(z0))))))
5(3(0(0(z0)))) → 5(0(4(3(0(2(z0))))))
5(1(0(3(2(z0))))) → 5(0(3(1(0(2(z0))))))
5(1(0(5(3(z0))))) → 5(5(0(1(3(1(z0))))))
5(1(3(0(0(z0))))) → 3(5(0(1(2(0(z0))))))
5(1(3(0(2(z0))))) → 3(0(2(1(5(2(z0))))))
5(1(3(0(2(z0))))) → 5(0(1(0(3(2(z0))))))
5(1(3(0(2(z0))))) → 5(0(1(1(2(3(z0))))))
5(1(3(2(0(z0))))) → 5(3(1(5(2(0(z0))))))
5(1(3(2(3(z0))))) → 3(4(3(5(1(2(z0))))))
5(1(4(5(2(z0))))) → 5(1(4(1(5(2(z0))))))
5(5(1(3(2(z0))))) → 3(5(5(4(1(2(z0))))))
Tuples:
0'(3(2(z0))) → c1(4'(3(0(2(z0)))), 0'(2(z0)))
0'(1(3(2(z0)))) → c4(0'(3(1(0(2(z0))))), 0'(2(z0)))
0'(1(3(2(z0)))) → c5(0'(2(z0)))
0'(1(3(2(z0)))) → c6(0'(1(4(3(1(2(z0)))))), 4'(3(1(2(z0)))))
5'(1(3(2(z0)))) → c36(0'(1(5(1(2(z0))))), 5'(1(2(z0))))
5'(1(3(2(z0)))) → c37(5'(2(2(z0))))
5'(1(3(2(3(z0))))) → c46(4'(3(5(1(2(z0))))), 5'(1(2(z0))))
S tuples:
0'(3(2(z0))) → c1(4'(3(0(2(z0)))), 0'(2(z0)))
0'(1(3(2(z0)))) → c4(0'(3(1(0(2(z0))))), 0'(2(z0)))
0'(1(3(2(z0)))) → c5(0'(2(z0)))
0'(1(3(2(z0)))) → c6(0'(1(4(3(1(2(z0)))))), 4'(3(1(2(z0)))))
5'(1(3(2(z0)))) → c36(0'(1(5(1(2(z0))))), 5'(1(2(z0))))
5'(1(3(2(z0)))) → c37(5'(2(2(z0))))
5'(1(3(2(3(z0))))) → c46(4'(3(5(1(2(z0))))), 5'(1(2(z0))))
K tuples:none
Defined Rule Symbols:
0, 4, 5
Defined Pair Symbols:
0', 5'
Compound Symbols:
c1, c4, c5, c6, c36, c37, c46
(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 7 of 7 dangling nodes:
0'(3(2(z0))) → c1(4'(3(0(2(z0)))), 0'(2(z0)))
5'(1(3(2(z0)))) → c37(5'(2(2(z0))))
0'(1(3(2(z0)))) → c4(0'(3(1(0(2(z0))))), 0'(2(z0)))
0'(1(3(2(z0)))) → c5(0'(2(z0)))
0'(1(3(2(z0)))) → c6(0'(1(4(3(1(2(z0)))))), 4'(3(1(2(z0)))))
5'(1(3(2(z0)))) → c36(0'(1(5(1(2(z0))))), 5'(1(2(z0))))
5'(1(3(2(3(z0))))) → c46(4'(3(5(1(2(z0))))), 5'(1(2(z0))))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(0(0(z0))) → 0(0(1(0(2(z0)))))
0(3(2(z0))) → 4(3(0(2(z0))))
0(0(4(2(z0)))) → 0(4(1(0(2(z0)))))
0(0(5(2(z0)))) → 5(0(2(3(0(z0)))))
0(1(3(2(z0)))) → 0(3(1(0(2(z0)))))
0(1(3(2(z0)))) → 3(1(1(0(2(z0)))))
0(1(3(2(z0)))) → 0(1(4(3(1(2(z0))))))
0(4(1(3(z0)))) → 1(4(3(0(2(2(z0))))))
0(4(2(3(z0)))) → 5(4(3(0(2(z0)))))
0(4(5(2(z0)))) → 5(0(2(2(4(2(z0))))))
0(5(1(3(z0)))) → 3(0(1(5(1(2(z0))))))
0(5(3(0(z0)))) → 5(0(1(4(3(0(z0))))))
0(5(3(2(z0)))) → 5(1(5(0(2(3(z0))))))
0(0(4(1(3(z0))))) → 4(0(1(0(2(3(z0))))))
0(0(4(5(2(z0))))) → 5(0(1(0(2(4(z0))))))
0(0(5(3(2(z0))))) → 0(1(5(0(2(3(z0))))))
0(1(0(5(2(z0))))) → 1(0(2(5(1(0(z0))))))
0(1(4(5(2(z0))))) → 2(1(5(0(2(4(z0))))))
0(3(1(4(0(z0))))) → 4(1(0(1(0(3(z0))))))
0(3(2(0(0(z0))))) → 0(0(1(0(2(3(z0))))))
0(3(4(0(2(z0))))) → 4(3(0(2(1(0(z0))))))
0(3(4(0(2(z0))))) → 4(3(0(2(3(0(z0))))))
0(3(4(4(2(z0))))) → 4(0(3(4(2(2(z0))))))
0(4(2(5(3(z0))))) → 0(4(3(5(1(2(z0))))))
0(5(1(2(0(z0))))) → 3(0(1(5(0(2(z0))))))
4(0(2(3(z0)))) → 3(4(3(0(2(z0)))))
4(0(2(3(z0)))) → 4(3(5(0(2(z0)))))
4(4(1(3(z0)))) → 4(3(4(1(2(2(z0))))))
4(5(2(0(z0)))) → 4(2(1(5(0(2(z0))))))
4(5(2(0(z0)))) → 5(1(0(2(2(4(z0))))))
4(4(2(2(0(z0))))) → 4(1(0(2(2(4(z0))))))
4(5(1(2(0(z0))))) → 5(0(4(1(2(2(z0))))))
4(5(2(3(2(z0))))) → 5(4(3(5(2(2(z0))))))
5(1(0(0(z0)))) → 5(1(0(2(0(z0)))))
5(1(0(0(z0)))) → 5(2(1(0(2(0(z0))))))
5(1(3(0(z0)))) → 5(0(2(1(3(z0)))))
5(1(3(2(z0)))) → 3(0(1(5(1(2(z0))))))
5(1(3(2(z0)))) → 3(1(1(5(2(2(z0))))))
5(3(0(0(z0)))) → 5(0(4(3(0(2(z0))))))
5(1(0(3(2(z0))))) → 5(0(3(1(0(2(z0))))))
5(1(0(5(3(z0))))) → 5(5(0(1(3(1(z0))))))
5(1(3(0(0(z0))))) → 3(5(0(1(2(0(z0))))))
5(1(3(0(2(z0))))) → 3(0(2(1(5(2(z0))))))
5(1(3(0(2(z0))))) → 5(0(1(0(3(2(z0))))))
5(1(3(0(2(z0))))) → 5(0(1(1(2(3(z0))))))
5(1(3(2(0(z0))))) → 5(3(1(5(2(0(z0))))))
5(1(3(2(3(z0))))) → 3(4(3(5(1(2(z0))))))
5(1(4(5(2(z0))))) → 5(1(4(1(5(2(z0))))))
5(5(1(3(2(z0))))) → 3(5(5(4(1(2(z0))))))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
0, 4, 5
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))